package srt.tool;

import srt.ast.AssertStmt;
import srt.ast.AssignStmt;
//Querry to z3 builder
public class SMTLIBQueryBuilder {

	private ExprToSmtlibVisitor exprConverter;
	private CollectConstraintsVisitor constraints;
	private String queryString = "";

	public SMTLIBQueryBuilder(CollectConstraintsVisitor ccv) {
		this.constraints = ccv;
		this.exprConverter = new ExprToSmtlibVisitor();
	}

	public void buildQuery() {
		StringBuilder query = new StringBuilder();
		query.append("\n\n(set-logic QF_BV)\n"
				+ "(define-fun tobv32 ((p Bool)) (_ BitVec 32) (ite p (_ bv1 32) (_ bv0 32)))\n");
		query.append("(define-fun tobool ((b (_ BitVec 32))) (Bool) (not (= b (_ bv0 32) )))\n"); //define tobool function

		//Declare variables
		for (String var : constraints.variableNames) {
			String line = "(declare-fun " + var + " () (_ BitVec 32))\n";
			query.append(line);
		}

		query.append(prepareOutputVariables());

		// Add constraints
		for (AssignStmt e : constraints.transitionNodes) {
			String line = "(assert ( = " + exprConverter.visit(e.getLhs()) + " "
					+ exprConverter.visit(e.getRhs()) + "))\n";
			query.append(line);
		}

		query.append(generateAssertions());

		query.append("(check-sat)\n");

		query.append(getOtputVariables());

		queryString = query.toString();
	}
	
	//generating assertions
	private String generateAssertions() {
		StringBuilder sb = new StringBuilder();
		if (constraints.propertyNodes.size() != 0) {

			sb.append("(assert( or");

			for (AssertStmt stm1 : this.constraints.propertyNodes) {
				sb.append("(not (tobool "
						+ exprConverter.visit(stm1.getCondition()) + "))");
			}
			sb.append("))\n");

		}
		return sb.toString();

	}
	
	//declaring of prop variables
	private String prepareOutputVariables() {

		StringBuilder sb = new StringBuilder();

		for (int i = 0; i < this.constraints.propertyNodes.size(); ++i) {
			String line = "(declare-fun prop" + i + " () (Bool))\n";
			sb.append(line);
			String line1 = "(assert (= prop"
					+ i
					+ " (not (tobool  "
					+ exprConverter.visit(constraints.propertyNodes.get(i)
							.getCondition()) + "))))\n";
			sb.append(line1);
		}

		return sb.toString();
	}

	//get value declaration
	private String getOtputVariables() {
		StringBuilder sb = new StringBuilder();

		sb.append("(get-value (");

		for (int i = 0; i < this.constraints.propertyNodes.size(); ++i) {
			sb.append(" prop" + i);
		}
		sb.append("))\n");

		return sb.toString();
	}

	public String getQuery() {
		return queryString;
	}

}
